package org.xteam.sled.semantic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.IExpRewriter;
import org.xteam.sled.semantic.exp.VariableSubstitute;


public class Sequence {
	
	private boolean hasPrefix = false;
	private boolean hasSuffix = false;
	private List<SequenceElement> elements = new ArrayList<SequenceElement>();
	
	public Sequence() {
	}
	
	public Sequence(SequenceElement cs) {
		elements.add(cs);
	}
	
	public Sequence(boolean hasPrefix, boolean hasSuffix,
			List<SequenceElement> elements) {
		this.hasPrefix = hasPrefix;
		this.hasSuffix = hasSuffix;
		this.elements = elements;
	}

	public List<SequenceElement> getElements() {
		return elements;
	}
	
	public boolean hasPrefix() {
		return hasPrefix;
	}
	
	public boolean hasSuffix() {
		return hasSuffix;
	}
	
	public void add(SequenceElement constraints) {
		elements.add(constraints);
	}
	
	public boolean isContradictory() {
		for (SequenceElement cnts :elements) {
			if (cnts.isContradictory())
				return true;
		}
		return false;
	}

	public int bitLength() {
		int l = 0;
		for (SequenceElement cnsts : elements) {
			l += cnsts.width();
		}
		return l;
	}
	
	public Sequence preDots() {
		return new Sequence(true, hasSuffix, new ArrayList<SequenceElement>(elements));
	}

	public Sequence postDost() {
		return new Sequence(hasPrefix, true, new ArrayList<SequenceElement>(elements));
	}
	
	public Sequence mergeLeft(Sequence other) {
		Sequence result = new Sequence();
		for (int i = 0; i < Math.max(elements.size(), other.elements.size()); ++i) {
			if (i >= elements.size()) {
				if (! hasSuffix)
					throw new RuntimeException("Shapes differ for &; left-hand sequence too short");
				result.add(other.elements.get(i));
			} else if (i >= other.elements.size()) {
				if (! other.hasSuffix)
					throw new RuntimeException("Shapes differ for &; right-hand sequence too short");
				result.add(elements.get(i));
			} else if (! (elements.get(i).isLabel() || other.elements.get(i).isLabel())) {
				result.add(((Constraints)elements.get(i)).merge((Constraints)other.elements.get(i)));
			} else {
			//| (label, SEQ_CONS _) => Seq.mkSequent label :: m(t1, seq2)
			//| (_,     label)      => Seq.mkSequent label :: m(seq1, t2)
				throw new RuntimeException("not completed");
			}
		}
		return result;
	}
	
	public Sequence mergeRight(Sequence other) {
		for (int i = Math.max(elements.size(), other.elements.size())-1; i >= 0; --i) {
			throw new RuntimeException("not completed");
		}
		return null;
	}
	
	public Map<String, Exp> labelOffsets() {
		Map<String, Exp> bindings = new HashMap<String, Exp>();
		int n = 0;
		for (SequenceElement element : getElements()) {
			if (element.isLabel()) {
				((Label) element).addBinding(bindings, n);
			} else {
				n += element.width();
			}
		}
		return bindings;
	}
	
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		if (hasPrefix) {
			buffer.append("...");
		}
		boolean isFirst = true;
		for (SequenceElement cnsts : elements) {
			if (isFirst)
				isFirst = false;
			else
				buffer.append("; ");
			buffer.append(cnsts.toString());
		}
		if (hasSuffix) {
			buffer.append("...");
		}
		return buffer.toString();
	}

	public void makePCRelative(VariableSubstitute subs) {
		Iterator<SequenceElement> i = elements.iterator();
		while (i.hasNext()) {
			SequenceElement element = i.next();
			if (element.isLabel() && ((Label)element).isActual()) {
				i.remove(); 
			} else {
				element.substitute(subs);
			}
		}
	}

	public Sequence subst(IExpRewriter subs) {
		List<SequenceElement> n = new ArrayList<SequenceElement>();
		for (SequenceElement e : elements) {
			n.add(e.substitute(subs));
		}
		return new Sequence(hasPrefix, hasSuffix, n);
	}

	public Sequence injectLatent() {
		List<SequenceElement> n = new ArrayList<SequenceElement>();
		for (SequenceElement e : elements) {
			n.add(e.injectLatent());
		}
		return new Sequence(hasPrefix, hasSuffix, n);
	}

	public Sequence actualize(boolean actualsOk) {
		List<SequenceElement> newElements = new ArrayList<SequenceElement>();
		for (SequenceElement element : elements) {
			newElements.add(element.actualize(actualsOk));
		}
		return new Sequence(hasPrefix, hasSuffix, newElements);
	}

}
